package edu.asu.sapa.ground;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Map;

/**
 * 
 * Change to share memory across states for Entry objects
 * 
 * Exploit advance to figure out copying?
 * 
 */

// modified copy of java.util.HashMap
public final class PropDB implements Cloneable {
	public final static class Entry {
		public static final int beforeValueMask = 0xC0000000;
		public static final int beforeValueShift = 30;
		public static final int atValueMask = 0x30000000;
		public static final int atValueShift = 28;
		public static final int afterValueMask = 0x0C000000;
		public static final int afterValueShift = 26;
		public static final int unsetMask = 0x0;
		public static final int trueMask = 0x1;
		public static final int falseMask = 0x2;
		public static final int undefMask = 0x3;
		
		public static final int lockMask = 0x02000000;
		
		public static final int advanceMask = 0x03FFFFF;
		public static final int valuesMask = 0xFC000000;
		
		public static final int defaultValueLock = 0x80000000;

		public int key;
		public int valueLock;
		public float time;

		public Entry() {
			this.key = -1;
			this.valueLock = defaultValueLock;
			this.time = Float.NEGATIVE_INFINITY;
		};

		public Entry(int key) {
			this.key = key;
			this.valueLock = defaultValueLock;
			this.time = Float.NEGATIVE_INFINITY;
		}
		
		public Entry(int key, int valueLock) {
			this.key = key;
			this.valueLock = valueLock;
			this.time = Float.NEGATIVE_INFINITY;
		}
		
		public Entry(int key, int valueLock, float time) {
			this.key = key;
			this.valueLock = valueLock;
			this.time = time;
		}

		public Entry(int key, float time) {
			this.key = key;
			this.valueLock = defaultValueLock;
			this.time = time;
		}

		public Entry(Entry e) {
			this.key = e.key;
			this.valueLock = e.valueLock;
			this.time = e.time;
		}

		private final boolean advanceBefore(float t) {
			if (t <= time) {
				return false;
			}
			time = t;
			int v = valueLock & afterValueMask;
			if (v != 0) {
				valueLock = (valueLock & advanceMask) | (v << 4);
				return true;
			}
			v = valueLock & atValueMask;
			if (v != 0) {
				valueLock = (valueLock & advanceMask) | (v << 2);
				return true;
			}
			return true;
		}
		private final boolean advanceAt(float t) {
			if (t > time) {
				time = t;
				int v = valueLock & afterValueMask;
				if (v != 0) {
					valueLock = (valueLock & advanceMask) | (v << 4) | (v << 2);
					return true;
				}
				v = valueLock & atValueMask;
				if (v != 0) {
					valueLock = (valueLock & advanceMask) | (v << 2) | v;
					return true;
				}
				valueLock |= (valueLock & beforeValueMask) >>> 2;
				return true;
			}
			if ((valueLock & atValueMask) == 0) {
				valueLock |= (valueLock & beforeValueMask) >>> 2;
				return true;
			} 
			return false;
		}
		private final boolean advanceAfter(float t) {
			if (t > time) {
				time = t;
				int v = valueLock & afterValueMask;
				if (v != 0) {
					valueLock = (valueLock & ~(beforeValueMask | atValueMask)) | (v << 4) | (v << 2);
					return true;
				}
				v = valueLock & atValueMask;
				if (v != 0) {
					valueLock = (valueLock & ~beforeValueMask) | (v << 2) | (v>>>2);
					return true;
				}
				v = valueLock & beforeValueMask;
				valueLock = valueLock | (v >>> 2) | (v >>> 4);
				return true;
			}
			if ((valueLock & afterValueMask) == 0) {
				int v = valueLock & atValueMask;
				if (v == 0) {
					v = valueLock & beforeValueMask;
					valueLock = valueLock | (v >>> 2) | (v >>> 4);
				} else {
					valueLock |= v >>> 2;
				}
				return true;
			} 
			return false;
		}
		private final void frameAt() {
			if ((valueLock & atValueMask) == 0) {
				valueLock |= (valueLock & beforeValueMask) >>> 2;
			} 
		}
		private final void frameAfter() {
			if ((valueLock & afterValueMask) == 0) {
				if ((valueLock & atValueMask) == 0) {
					valueLock |= (valueLock & beforeValueMask) >>> 2;
				} 
				valueLock |= (valueLock & atValueMask) >>> 2;
			} 
		}
		public final int getValueBefore() {
			return (valueLock & beforeValueMask) >>> beforeValueShift;
		}
		public final boolean getValueBefore(boolean value) {
			return ((valueLock & beforeValueMask) >>> beforeValueShift) == (value ? trueMask : falseMask);
		}
		public boolean getValueBefore(float time, boolean b) {
			if (time > this.time)
				return getValueAfter(b);
			return getValueBefore(b);
		}
		public final int getValueAt() {
			if ((valueLock & atValueMask) == 0)
				return (valueLock & beforeValueMask) >>> beforeValueShift;
			return (valueLock & atValueMask) >>> atValueShift;
		}
		public final boolean getValueAt(boolean value) {
			if ((valueLock & atValueMask) == 0)
				return ((valueLock & beforeValueMask) >>> beforeValueShift) == (value ? trueMask : falseMask);
			return ((valueLock & atValueMask) >>> atValueShift) == (value ? trueMask : falseMask);
		}
		public boolean getValueAt(float time, boolean b) {
			if (time > this.time)
				return getValueAfter(b);
			return getValueAt(b);
		}
		public final int getValueAfter() {
			if ((valueLock & afterValueMask) == 0)
				if ((valueLock & atValueMask) == 0)
					return ((valueLock & beforeValueMask) >>> beforeValueShift);
				else
					return ((valueLock & atValueMask) >>> atValueShift);
			else
				return ((valueLock & afterValueMask) >>> afterValueShift);
		}
		public final boolean getValueAfter(boolean value) {
			if ((valueLock & afterValueMask) == 0)
				if ((valueLock & atValueMask) == 0)
					return ((valueLock & beforeValueMask) >>> beforeValueShift) == (value ? trueMask : falseMask);
				else
					return ((valueLock & atValueMask) >>> atValueShift) == (value ? trueMask : falseMask);
			else
				return ((valueLock & afterValueMask) >>> afterValueShift) == (value ? trueMask : falseMask);
		}
		private final int readValueBefore(float t) {
			advanceBefore(t);
			return (valueLock & beforeValueMask) >>> beforeValueShift;
		}
		private final int readValueAt(float t) {
			advanceAt(t);
			return (valueLock & atValueMask) >>> atValueShift;
		}
		/* shouldn't be writing before or reading after */
		@Deprecated
		private final int readValueAfter(float t) {
			advanceAfter(t);
			return (valueLock & afterValueMask) >>> afterValueShift;
		}
		private final boolean readValueBefore(float time, boolean value) {
			advanceBefore(time);
			return ((valueLock & beforeValueMask) >>> beforeValueShift) == (value ? trueMask : falseMask);
		}
		private final boolean readValueAt(float time, boolean value) {
			advanceAt(time);
			return (valueLock & atValueMask) >>> atValueShift == (value ? trueMask : falseMask);
		}

		private final boolean undefineAt(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | (undefMask << atValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean undefineAtInstant(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | (undefMask << atValueShift);
				return true;
			} 
			return false;
		}
		private final boolean undefineAfter(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & afterValueMask) == 0) {
				valueLock = valueLock | (undefMask << afterValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean setTrueAt(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | (trueMask << atValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean setFalseAt(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | (falseMask << atValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean setAt(float t, boolean value) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | ((value ? trueMask : falseMask) << atValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean setTrueAtInstant(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | (trueMask << atValueShift);
				return true;
			} 
			return false;
		}
		private final boolean setFalseAtInstant(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | (falseMask << atValueShift);
				return true;
			} 
			return false;
		}
		private final boolean setAtInstant(float t, boolean value) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & atValueMask) == 0) {
				valueLock = valueLock | ((value ? trueMask : falseMask) << atValueShift);
				return true;
			} 
			return false;
		}
		private final boolean setTrueAfter(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & afterValueMask) == 0) {
				valueLock = valueLock | (trueMask << afterValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean setFalseAfter(float t) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & afterValueMask) == 0) {
				valueLock = valueLock | (falseMask << afterValueShift) | lockMask;
				return true;
			} 
			return false;
		}
		private final boolean setAfter(float t, boolean value) {
			if ((valueLock & lockMask) != 0) {
				return false;
			}
			if (advanceBefore(t) || (valueLock & afterValueMask) == 0) {
				valueLock = valueLock | ((value ? trueMask : falseMask) << afterValueShift) | lockMask;
				return true;
			} 
			return false;
		}


		public final int getLock() {
			return valueLock & lockMask;
		}

		public final boolean unLocked() {
			return ((valueLock & lockMask) == 0);
		}

		private final boolean lock(float time) {
			advanceBefore(time);
			int l = valueLock & lockMask;
			if (l == 0) {
				valueLock |= lockMask;
				return true;
			}
			return false;
		}

		private final boolean unlock(float time) {
			advanceBefore(time);
			int l = valueLock & lockMask;
			if (l != 0) {
				valueLock &= ~lockMask;
				return true;
			}
			return false;
		}
		
		public final boolean writableAt(float t) {
			if ((valueLock & lockMask) != 0)
				return false;
			if (t > time || (valueLock & atValueMask) == 0)
				return true;
			return false;
		}
		
		public final boolean writableAfter(float t) {
			if ((valueLock & lockMask) != 0)
				return false;
			if (t > time || (valueLock & afterValueMask) == 0)
				return true;
			return false;
		}

		/**
		 * Does not verify that u and v are both unlocked.  Only meant to be applied to PropDBs at steady states.
		 * (no future events except at infinity [goals])
		 * 
		 * @param u - a valueLock
		 * @param v - a valueLock
		 * @return Whether or not u and v represent the same assignment as far as the present + future are concerned
		 */
		public static boolean equals(int u, int v) {
			int a1, a2;
			a1 = u & afterValueMask;
			a2 = v & afterValueMask;
			if (a1 != a2)
				return false;
			if (a1 == 0) {
				a1 = u & atValueMask;
				a2 = v & atValueMask;
				if (a1 != a2)
					return false;
				if (a1 == 0) {
					a1 = u & beforeValueMask;
					a2 = v & beforeValueMask;
					if (a1 != a2)
						return false;
				}
			}
			return true;
		}
	}

	/**
	 * The default initial capacity - MUST be a power of two.
	 */
	static final int DEFAULT_INITIAL_CAPACITY = 16;

	/**
	 * The table, resized as necessary. Length MUST Always be a power of two.
	 */
	public Entry[] table;

	/**
	 * The number of key-value mappings contained in this map.
	 */
	public int size;

	public PropDB() {
		table = new Entry[DEFAULT_INITIAL_CAPACITY];
		size = 0;
	}

	public PropDB(int initialCapacity) {
		if (initialCapacity <= 0)
			throw new IllegalArgumentException("Illegal initial capacity: "
					+ initialCapacity);

		int capacity = Integer.highestOneBit(initialCapacity);
		if (capacity < initialCapacity)
			capacity <<= 1;

		table = new Entry[capacity];
		size = 0;
	}

	public PropDB(PropDB m) {
		int s = m.size;
		int capacity = Integer.highestOneBit(s);
		if (capacity < s)
			capacity <<= 1;
		Entry[] tbl = new Entry[capacity];
		table = tbl;
		size = 0;
		Entry[] src = m.table;
		createAllInternal(tbl, capacity, src, src.length);
	}

	// internal utilities

	// this doesn't quite work right, because propDB is blind to advance() 
	@Override
	public int hashCode() {
		int result = 0;
		Entry[] tbl = table;
		int l = tbl.length;
		int i;
		Entry e;
		//3,6,9,12(C)
		//1,2
		//4,8
		//14(E),13(D)
		//11(B),7
		
		// use an LSFR to select these to fit into the gaps?
		/*int[] p = {1,2,4,8};
		int[] q = {0xE,0xD,0XB,7};
		int n=0;
		*/
		
		for(i=0;i<l;++i) {
			e = tbl[i];
			if (e == null)
				continue;
			int v = e.valueLock;
			if ((v & 0x54000000) != 0) {
				// the max value of key is the number of propositions.
				// more than 512 propositions is unlikely
				// for that matter, more than 256 propositions is also unlikely
				// need to get a good balance of 0 and 1 bits for the accumulating XOR
				// which has the effect of counting, in each bit, some subset of the propositions that are
				// true (or undefined) before, at, or after the current time.  (the meaning of 0x54000000)
				// where ''some subset'' is determined by the calculation of h
				int k = e.key;
				// a,b,c,d are the values 1-4, shifted up by various amounts
				int a = (k & 0xC0) + 0x40;
				int b = (k & 0x30) + 0x10;
				int c = (k & 0x0C) + 0x04;
				int d = (k & 0x03) + 0x01;
				int h;
				int s = (k>>>6)&(28);
				// this multiplies each of a,b,c,d by 3, and packs them into an integer, circularly shifted
				// by the higher bits of k, along with a fixed pattern that changes as k increases
				// one could use the yet higher bits of k to select between the given patterns; but
				// a problem that gets to case 2 has grounded more than 512 propositions...
				switch(s>>>2) {
				case 0:
					h = ((a<<22) + (a<<23))
					  | ((b<<16) + (b<<17))
					  | ((c<<10) + (c<<11))
					  | ((d<<4 ) + (d<<5 ))
					  | 0x010E010E
					  ;
					break;
				case 1:
					h = ((a<<18) + (a<<19))
					  | ((b<<12) + (b<<13))
					  | ((c<<6 ) + (c<<7 ))
					  | ((d    ) + (d<<1 ))
					  | 0xE010E010
					  ;
				case 2:
					h = ((a<<14) + (a<<15))
					  | ((b<<8 ) + (b<<9 ))
					  | ((c<<2 ) + (c<<3 ))
					  | ((d<<28) + (d<<29))
					  | 0x0D020D02
					  ;
				case 3:
					h = ((a<<10) + (a<<11))
					  | ((b<<4 ) + (b<<5 ))
					  | ((c>>>2) + (c>>>1))
					  | ((d<<24) + (d<<25))
					  | 0x20D020D0
					  ;
				case 4:
					h = ((a<<6 ) + (a<<7 ))
					  | ((b    ) + (b<<1 ))
					  | ((c<<26) + (c<<27))
					  | ((d<<20) + (d<<21))
					  | 0x040B040B
					  ;
				case 5:
					h = ((a<<2 ) + (a<<3 ))
					  | ((b>>>4) + (b>>>3))
					  | ((c<<22) + (c<<23))
					  | ((d<<16) + (d<<17))
					  | 0xB040B040
					  ;
				case 6:
					h = ((a>>>2) + (a>>>1))
					  | ((b<<24) + (b<<25))
					  | ((c<<18) + (c<<19))
					  | ((d<<12) + (d<<13))
					  | 0x07080708
					  ;
				case 7:
				default:
					h = ((a>>>6) + (a>>>5))
					  | ((b<<20) + (b<<21))
					  | ((c<<14) + (c<<15))
					  | ((d<<8) + (d<<9))
					  | 0x80708070
					  ;
				}
				// This has the effect of segmenting propositions into blocks of 256, none of which collide with each other, 
				// for that matter, no two propositions collide with a third in the same block in any of the 4 components, 
				// so it takes a group of, at least, 4 propositions to collide in 1 one component, and a full collision of course requires
				// collisions in all 4 components.  There are such sets, in base 4, 0000 1111 2222 and 3333 collide.  Similarly 0101 1212, 2323, and 3030 collide.
				// This could be improved to needing 5 propositions to induce a collision in 1 component (as there are 4 bits)
				// but that would require (at least) one of the bit patterns to have an odd number of bits set.
				// The 0x010E010E pattern ensures that sets of propositions which are 256 apart only rarely collide; 
				// by using only even bits for the dynamic portion of h it is guaranteed that the running XOR always has even bits set 
				// for the dynamic portion.  The only way then to collide at 256 apart is to induce even bits in the fixed portion of the patterns,
				// which only happens for even sets, and is the value 0 in each component.  So the only collisions on sets that are 256 apart is
				// on 0.  
				// States which differ in exactly one proposition cannot collide -- h is non-zero for every id, and so the running XOR
				// after the common part is of course identical, and then the one extra proposition changes the parity of half of the bits.
				// States which differ in exactly two propositions are still unlikely to collide, as the one has to be a direct collision with
				// the other.  That can only happen for key and key+m*2048.
				// In short, the XOR of the symmetric difference of states has to be 0 in order for states to collide.  That requires at least 4
				// propositions within the same group of 256, and it doesn't help to use a 512 range since the two 256 sub-ranges would have to individually
				// XOR to 0, requiring 4 propositions in each 256 block.  One might even be able to show that the size of the symmetric difference
				// has to be 0 mod 4 in order for a collision to occur.  
				result ^= h;
				//result = 31 * result + e.key;
				//result *= e.key + 1;
			}
		}
		//return result;
		return result*((size<<1)+1);
	}

	/**
	 * Applies a supplemental hash function to a given hashCode, which defends
	 * against poor quality hash functions. This is critical because HashMap
	 * uses power-of-two length hash tables, that otherwise encounter collisions
	 * for hashCodes that do not differ in lower bits. Note: Null keys always
	 * map to hash 0, thus index 0.
	 */
	static final int hash(int h) {
		h ^= (h >>> 20) ^ (h >>> 12);
		return h ^ (h >>> 7) ^ (h >>> 4);
	}

	public int size() {
		return size;
	}

	public boolean isEmpty() {
		return size == 0;
	}

	Entry getInternal(int key) {
		int hash = hash(key);
		Entry[] tbl = table;
		int l = tbl.length;
		int index = hash & (l - 1);
		int i = index;
		Entry entry = tbl[i];
		if (entry == null)
			return null;
		if (entry.key == key)
			return entry;
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null)
				return null;
			if (entry.key == key)
				return entry;
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null)
				return null;
			if (entry.key == key)
				return entry;
		}
		return null;
	}
	
	Entry getInternalCopy(int key) {
		int hash = hash(key);
		Entry[] tbl = table;
		int l = tbl.length;
		int index = hash & (l - 1);
		int i = index;
		Entry entry = tbl[i];
		if (entry == null)
			return null;
		if (entry.key == key)
			return tbl[i] = new Entry(entry);
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null)
				return null;
			if (entry.key == key)
				return tbl[i] = new Entry(entry);
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null)
				return null;
			if (entry.key == key)
				return tbl[i] = new Entry(entry);
		}
		return null;
	}
	
	int getIndex(int key) {
		int hash = hash(key);
		Entry[] tbl = table;
		int l = tbl.length;
		int index = hash & (l - 1);
		int i = index;
		Entry entry = tbl[i];
		if (entry == null || entry.key == key)
			return i;
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null || entry.key == key)
				return i;
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null || entry.key == key)
				return i;
		}
		return -1;
	}

	
	// always makes a new Entry object
	public Entry get(int key) {
		int hash = hash(key);
		Entry[] tbl = table;
		int l = tbl.length;
		int index = hash & (l - 1);
		int i = index;
		Entry entry = tbl[i];
		if (entry == null)
			return tbl[i] = new Entry(key);
		if (entry.key == key)
			return tbl[i] = new Entry(entry);
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null)
				return tbl[i] = new Entry(key);
			if (entry.key == key)
				return tbl[i] = new Entry(entry);
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null)
				return tbl[i] = new Entry(key);
			if (entry.key == key)
				return tbl[i] = new Entry(entry);
		}
		grow();
		return get(key);
	}

	/**
	 * 
	 * valueLock needs to be non-default
	 * 
	 * @param key
	 * @param valueLock
	 * @return Returns the new/modified Entry
	 */
	public Entry put(int key, int valueLock, float time) {
		int hash = hash(key);
		Entry[] tbl = table;
		int l = tbl.length;
		int t = l >> 1 + l >> 2;
		if (size > t)
			l = grow();
		int index = hash & (l - 1);
		int i=index;
		Entry entry = tbl[i];
		if (entry == null) {
			tbl[i] = entry = new Entry(key, valueLock, time);
			++size;
			return entry;
		}
		if (entry.key == key) {
			if (entry.valueLock == Entry.defaultValueLock)
				++size;
			return tbl[i] = new Entry(key,valueLock,time);
		}
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = entry = new Entry(key, valueLock, time);
				++size;
				return entry;
			}
			if (entry.key == key) {
				if (entry.valueLock == Entry.defaultValueLock)
					++size;
				return tbl[i] = new Entry(key,valueLock,time);
			}
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = entry = new Entry(key, valueLock, time);
				++size;
				return entry;
			}
			if (entry.key == key) {
				if (entry.valueLock == Entry.defaultValueLock)
					++size;
				return tbl[i] = new Entry(key,valueLock,time);
			}
		}

		l = grow();
		return putInternal(key, new Entry(key,valueLock,time), tbl, l);
	}

	Entry putInternal(Entry e, Entry[] tbl, int l) {
		int key = e.key;
		int i;
		int hash = hash(key);
		int index = hash & (l - 1);
		i = index;
		Entry entry = tbl[i];
		if (entry == null) {
			tbl[i] = e;
			++size;
			return e;
		}
		if (entry.key == key) {
			if (entry.valueLock == Entry.defaultValueLock)
				++size;
			return tbl[i] = e;
		}
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = e;
				++size;
				return e;
			}
			if (entry.key == key) {
				if (entry.valueLock == Entry.defaultValueLock)
					++size;
				return tbl[i] = e;
			}
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = e;
				++size;
				return e;
			}
			if (entry.key == key) {
				if (entry.valueLock == Entry.defaultValueLock)
					++size;
				return tbl[i] = e;
			}
		}

		l = grow();
		return putInternal(key, e, tbl, l);
	}
	
	Entry putInternal(int key, Entry e, Entry[] tbl, int l) {
		int i;
		int hash = hash(key);
		int index = hash & (l - 1);
		i = index;
		Entry entry = tbl[i];
		if (entry == null) {
			tbl[i] = e;
			++size;
			return e;
		}
		if (entry.key == key) {
			if (entry.valueLock == Entry.defaultValueLock)
				++size;
			return tbl[i] = e;
		}
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = e;
				++size;
				return e;
			}
			if (entry.key == key) {
				if (entry.valueLock == Entry.defaultValueLock)
					++size;
				return tbl[i] = e;
			}
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = e;
				++size;
				return e;
			}
			if (entry.key == key) {
				if (entry.valueLock == Entry.defaultValueLock)
					++size;
				return tbl[i] = e;
			}
		}

		l = grow();
		return putInternal(key, e, tbl, l);
	}

	Entry removeInternal(int key, Entry[] tbl, int l) {
		int i;
		int hash = hash(key);
		int index = hash & (l - 1);
		i = index;
		Entry entry = tbl[i];
		if (entry == null) {
			tbl[i] = entry = new Entry(key);
			return entry;
		}
		if (entry.key == key) {
			if (entry.valueLock != Entry.defaultValueLock)
				--size;
			return tbl[i] = new Entry(key);
		}
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = entry = new Entry(key);
				return entry;
			}
			if (entry.key == key) {
				if (entry.valueLock != Entry.defaultValueLock)
					--size;
				return tbl[i] = new Entry(key);
			}
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = entry = new Entry(key);
				return entry;
			}
			if (entry.key == key) {
				if (entry.valueLock != Entry.defaultValueLock)
					--size;
				return tbl[i] = new Entry(key);
			}
		}

		l = grow();
		return removeInternal(key, tbl, l);
	}

	void putAllInternal(Entry[] tbl, int l, Entry[] src, int s) {
		for (int i = 0; i < s; ++i) {
			Entry e = src[i];
			if (e != null) {
				int v = e.valueLock;
				if (v != Entry.defaultValueLock)
					putInternal(e, tbl, l);
			}
		}
	}
	
	
	void createAllInternal(Entry[] tbl, int l, Entry[] src, int s) {
		for (int i = 0; i < s; ++i) {
			Entry e = src[i];
			if (e != null) {
				int v = e.valueLock;
				if (v != Entry.defaultValueLock)
					createInternal(e, tbl, l);
			}
		}
	}
	
	void createInternal(Entry e, Entry[] tbl, int l) {
		int key = e.key;
		int i;
		int hash = hash(key);
		int index = hash & (l - 1);
		i = index;
		Entry entry = tbl[i];
		if (entry == null) {
			tbl[i] = e;
			++size;
			return;
		}
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = e;
				++size;
				return;
			}
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = e;
				++size;
				return;
			}
		}

		System.err.println("Programming error");
	}

	int grow() {
		Entry[] oldTable = table;
		int l = oldTable.length;
		int s = l << 1;
		Entry[] newTable = new Entry[s];
		table = newTable;
		size = 0;
		createAllInternal(newTable, s, oldTable, l);
		return s;
	}

	void grow(int s) {
		Entry[] oldTable = table;
		int l = oldTable.length;
		Entry[] newTable = new Entry[s];
		table = newTable;
		size = 0;
		createAllInternal(newTable, s, oldTable, l);
	}

	public void putAll(PropDB m) {
		int l = m.size;
		if (l == 0)
			return;
		Entry[] tbl = table;
		int s = tbl.length;
		if (l > s) {
			s = Integer.highestOneBit(l);
			if (s < l)
				s <<= 1;
			grow(s);
			tbl = table;
		}

		Entry[] src = m.table;
		int sz = src.length;
		putAllInternal(tbl, s, src, sz);
	}

	/**
	 * @param key
	 *          proposition id to be set to false (/removed)
	 * 
	 */
	public Entry remove(int key) {
		int i;
		int hash = hash(key);
		Entry[] tbl = table;
		int l = tbl.length;
		int index = hash & (l - 1);
		i = index;
		Entry entry = tbl[i];
		if (entry == null) {
			tbl[i] = entry = new Entry(key);
			return entry;
		}
		if (entry.key == key) {
			if (entry.valueLock != Entry.defaultValueLock)
				--size;
			return tbl[i] = new Entry(key);
		}
		for (i = index + 1; i < l; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = entry = new Entry(key);
				return entry;
			}
			if (entry.key == key) {
				if (entry.valueLock != Entry.defaultValueLock)
					--size;
				return tbl[i] = new Entry(key);
			}
		}
		for (i = 0; i < index; ++i) {
			entry = tbl[i];
			if (entry == null) {
				tbl[i] = entry = new Entry(key);
				return entry;
			}
			if (entry.key == key) {
				if (entry.valueLock != Entry.defaultValueLock)
					--size;
				return tbl[i] = new Entry(key);
			}
		}

		l = grow();
		return removeInternal(key, tbl, l);
	}

	public void clear() {
		Entry[] tbl = table;
		int l = tbl.length;
		for (int i = 0; i < l; ++i) {
			tbl[i] = null;
		}
		size = 0;
	}

	/**
	 * @return Deep copy
	 */
	public PropDB clone() {
		Entry[] tbl = table;
		int l = tbl.length;
		PropDB result = new PropDB(l);
		result.createAllInternal(result.table, l, tbl, l);

		return result;
	}

	// only valid if there is nothing to advance to, i.e., everything is
	// unlocked
	public final boolean equals(PropDB q) {
		Entry[] tbl = table;
		int s = table.length;
		if (size != q.size)
			return false;
		int i;
		Entry a, b;
		int u,v;
		for (i = 0; i < s; ++i) {
			a = tbl[i];
			if (a == null) 
				continue;
			u = a.valueLock;
			if (u == Entry.defaultValueLock)
				continue;
			b = q.getInternal(a.key);
			if (b == null)//!Entry.equals(a.valueLock,b.valueLock))
				return false;
			v = b.valueLock;
//			if (a.getValueAfter() != b.getValueAfter())
//				return false;
			if (u != v)
				return false;
		}
		return true;
	}

	public final boolean setAt(int id, boolean value, float time) {
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.setAt(time,value);
	}
	public final boolean setAt(Entry e, boolean value, float time) {
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.setAt(time,value);
	}
	public final boolean setAfter(int id, boolean value, float time) {
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.setAfter(time,value);
	}
	public final boolean setAfter(Entry e, boolean value, float time) {
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.setAfter(time,value);
	}
	public final boolean undefineAt(Entry e, float time) {
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.undefineAt(time);
	}
	public final boolean undefineAt(int id, float time) {
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.undefineAt(time);
	}
	public final boolean undefineAfter(Entry e, float time) {
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.undefineAt(time);
	}
	public final boolean undefineAfter(int id, float time) {
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.undefineAt(time);
	}

	public final boolean setAtInstant(Entry e, boolean value, float time) {
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.setAtInstant(time,value);
	}

	public final boolean setAtInstant(int id, boolean value, float time) {
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.setAtInstant(time,value);
	}

	public final boolean getValueBefore(int id, float time, boolean value) {
		Entry e = getInternal(id);
		if (e == null)
			return value == false;
		return e.getValueBefore(time,value);
	}
	public final boolean getValueAt(int id, float time, boolean value) {
		Entry e = getInternal(id);
		if (e == null)
			return value == false;
		return e.getValueAt(time,value);
	}
	public final boolean readValueBefore(int id, float time, boolean value) {
		Entry f;
		int i = getIndex(id);
		if (i < 0) {
			if (value)
				return false;
			return true;
		}
		Entry e = table[i];
		if (e == null) {
			if (value)
				return false;
			return true;
		}
		table[i] = f = new Entry(e);
		boolean possible = f.readValueBefore(time,value);
		size(e.valueLock,f.valueLock);
		return possible;
	}
	
	public final boolean readValueAt(int id, float time, boolean value) {
		Entry f;
		int i = getIndex(id);
		if (i < 0) {
			if (value)
				return false;
			grow();
			f = get(id);
			f.readValueAt(time,false);
			++size;
			return true;
		}
		Entry e = table[i];
		if (e == null) {
			if (value)
				return false;
			table[i] = f = new Entry(id,time);
			f.readValueAt(time,false);
			++size;
			return true;
		}
		table[i] = f = new Entry(e);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return f.readValueAt(time,value);
	}
	public final boolean readValueBefore(Entry e, float time, boolean value) {
		if (e.valueLock == Entry.defaultValueLock)
			return value == false;
		boolean possible = e.readValueBefore(time,value);
		if (e.valueLock == Entry.defaultValueLock)
			--size;
		return possible;
	}
	public final boolean readValueAt(Entry e, float time, boolean value) {
		int u = e.valueLock;
		boolean possible = e.readValueAt(time,value);
		int v = e.valueLock;
		size(u,v);
		return possible;
	}
	public final boolean writableAt(int id, float time) {
		Entry e = getInternal(id);
		if (e == null)
			return true;
		return e.writableAt(time);
	}
	public final boolean writableAfter(int id, float time) {
		Entry e = getInternal(id);
		if (e == null)
			return true;
		return e.writableAt(time);
	}
	public final boolean writableAt(Entry e, float time) {
		return e.writableAt(time);
	}
	public final boolean writableAfter(Entry e, float time) {
		return e.writableAt(time);
	}

	
	public String toString() {
		StringBuilder buf = new StringBuilder();
			Entry[] tbl = table;
			int s = table.length;
			int i;
			Entry a, b;
			for (i = 0; i < s; ++i) {
				a = tbl[i];
				if (a == null || a.valueLock == Entry.defaultValueLock) 
					continue;
				buf.append("(at ").append(a.time).append(" (= ").append(a.key).append(" ");
				if (a.getValueAt(true)) {
					buf.append("true))\n");
				} else if (a.getValueAt(false)) {
					buf.append("false))\n");
				} else {
					buf.append("undefined))\n");
				}
			}
		return buf.toString();
	}

	public boolean unlock(int id, float time) {
		Entry e = get(id);
		int v = e.valueLock;
		boolean possible = e.unlock(time);
		size(v,e.valueLock);
		return possible;
	}
	public boolean unlock(Entry e, float time) {
		int v = e.valueLock;
		boolean possible = e.unlock(time);
		size(v,e.valueLock);
		return possible;
	}

	public boolean unlockSetAtInstant(Entry e, float time, boolean value) {
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.unlock(time) && e.setAtInstant(time,value);
	}
	public boolean unlockSetAtInstant(int id, float time, boolean value) {
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.unlock(time) && e.setAtInstant(time,value);
	}
	
	private final void size(int u, int v) {
		if (u == Entry.defaultValueLock && v != Entry.defaultValueLock)
			++size;
		else if (u != Entry.defaultValueLock && v == Entry.defaultValueLock)
			--size;
	}

	public final Entry probe(int id) {
		return getInternal(id);
	}

	public final boolean readBeforeSetAtInstant(int id, float time, boolean value, boolean writeValue) {
		if (value) {
			Entry e = getInternalCopy(id);
			if (e == null || e.readValueBefore(time) != Entry.trueMask)
				return false;
			return e.setAtInstant(time,writeValue);
		}
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.readValueBefore(time) == Entry.falseMask && e.setAtInstant(time,writeValue);
	}

	public boolean readBeforeSetAt(int id, float time, boolean value, boolean writeValue) {
		if (value) {
			Entry e = getInternalCopy(id);
			if (e == null || e.readValueBefore(time) != Entry.trueMask)
				return false;
			return e.setAt(time,writeValue);
		}
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.readValueBefore(time) == Entry.falseMask && e.setAt(time,writeValue);
	}
	public boolean readAtSetAfter(int id, float time, boolean value, boolean writeValue) {
		if (value) {
			Entry e = getInternalCopy(id);
			if (e == null || e.readValueAt(time) != Entry.trueMask)
				return false;
			return e.setAfter(time,writeValue);
		}
		Entry e = get(id);
		if (e.valueLock == Entry.defaultValueLock)
			++size;
		return e.readValueAt(time) == Entry.falseMask && e.setAfter(time,writeValue);
	}
}
